line: lineCount - 1,

        ch: doc.getLine(lineCount - 1).length - 1

      }) + 1;

​

      if (this._validLead + this._validTrail === this._retrievedText.length

         && this._retrievedText.length === totalLength)

        return this._retrievedText;

​

      if (this._validLead + this._validTrail < totalLength / 4) { // if more than 0.75 of the document is modified

        this._retrievedText = doc.getValue();

        this._validLead = -1;

        return this._retrievedText;

      }

​

      var mid = doc.getRange(

        doc.posFromIndex(this._validLead),

        doc.posFromIndex(totalLength - this._validTrail));

      this._retrievedText =

        this._retrievedText.slice(0, this._validLead) +

        mid +

        this._retrievedText.slice(this._retrievedText.length - this._validTrail);

      this._validLead = -1;

      return this._retrievedText;

    }

​

    private _docChanges(docChanges: CodeMirror.EditorChange[]) {

​

      var doc = this.textDoc.doc;

​

      var lineCount = doc.lineCount();

      var totalLength = doc.indexFromPos({

        line: lineCount - 1,

        ch: doc.getLine(lineCount - 1).length - 1

      });

​

      for (var i = 0; i < docChanges.length; i++) {

        var ch = docChanges[i];

        var fromIndex = doc.indexFromPos(ch.from);

        var toIndex = doc.indexFromPos(ch.to);

        var trail = totalLength - toIndex;

        if (this._validLead < 0) {

          this._validLead = fromIndex;

          this._validTrail = trail;

        }

        else {

          this._validLead = Math.min(this._validLead, fromIndex);

          this._validTrail = Math.min(this._validTrail, trail);

        }

​

      }

      if (this.textDoc.onChanges)

        this.textDoc.onChanges(docChanges);

​

      if (this._scrollerModel)

        this._scrollerModel.docChanges(docChanges);

​

      this._saveTimer.interval = (this.moduleObj && this.moduleObj.saveDelay) || saveDelay;

      this._saveTimer.reset();

​

    }

​

    private _cursorActivity() {

      if (this.textDoc.onCursorMoved) {

        var cursorPos = this.textDoc.doc.getCursor();

        //this.textDoc.status.textContent = 'token '+this.textDoc.editor.getTokenAt(cursorPos).type;